Nuprl Lemma : multiply_functionality_wrt_le
13,42
postcript
pdf
i1
,
i2
,
j1
,
j2
:
. (
i1
j1
)
(
i2
j2
)
((
i1
*
i2
)
(
j1
*
j2
))
latex
Up
int
2
,
int
2
Definitions
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
False
,
A
,
A
B
,
,
Lemmas
nat
wf
,
le
wf
,
mul
preserves
le
origin